Nuprl Definition : on_maybe_hyp_tactic
13,42
postcript
pdf
REF, NoConds
on_maybe_hyp{ABS:q, $h:n}(
ident
;
tactic
) == OnHypMaybe (first_nat $h:n)
ident
(\h.
tactic
)
latex
Up
Tactics as terms
Definitions
OnMaybeHyp $h (\h.
tactic
)
FDL editor aliases
on-hyp
origin
